Nuprl Lemma : fpf-dom-list_wf
11,40
postcript
pdf
A
:Type,
eq
:EqDecider(
A
),
f
:
a
:
A
fp
Top. fpf-dom-list(
f
)
({
a
:
A
|
a
dom(
f
)} List)
latex
Definitions
x
.
t
(
x
)
,
t
.1
,
fpf-dom-list(
f
)
,
x
dom(
f
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
P
&
Q
,
P
Q
,
P
Q
,
,
P
Q
,
a
:
A
fp
B
(
a
)
Lemmas
deq
wf
,
top
wf
,
fpf
wf
,
assert-deq-member
,
deq-member
wf
,
assert
wf
,
l
member
wf
,
subtype
rel
list
,
list-set-type
origin
A:Type, eq:EqDecider(A), f:a:A fp
Top. fpf-dom-list(f) 
({a:A| 
a dom(f)} List) A:Type, eq:EqDecider(A), f:a:A fp Top. fpf-dom-list(f) ({a:A| a dom(f)} List) 
x. t(x) dom(f) Tx:A. B(x)
Q Q
Q B(a)